package alloy.symm;


import java.util.Collections;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.ElemFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.Expr;
import alloy.ast.Leaf;
import alloy.ast.LeafId;

/**
 * Find pairs of relations (r1,r2) that are definitely constrained to be disjoint in any solution.
 * We find top-level conjuncts of the form <code>no (...+r1+...) & ( ... +r2+...)
 */
class DisjDetector_V extends TopLevelConjVisitor {
    /**
     * Map from {@link LeafId} of a relation to a {@link Set} of LeafId's of relations with which
     * this relation is definitely disjoint.
     */
    private Map /* LeafId->Set[LeafId] */ _disjWith = new TreeMap();
    
    //--------//
    // Methods//
    //--------//
    
    DisjDetector_V() { }

    /** Test whether two relations are disjoint.  Call this after the visitor has walked the translatable AST. */
    boolean relationsAreDisjoint(LeafId r1_, LeafId r2_) {
	Set /* LeafId->Set[LeafId] */ r1DisjWith = (Set)_disjWith.get(r1_);
	if (r1DisjWith!=null && r1DisjWith.contains(r2_))
	    return true;
	return false;
    }

    /** Return the set of leaf ids of relations that are disjoint with the given relation. */
    Set /* of LeafId */ getRelsDisjFrom(LeafId r_) {
	Set /* of LeafId */ disjFromR = (Set)_disjWith.get(r_);
	return disjFromR != null ? disjFromR : Collections.EMPTY_SET;
    }
    
    /**
     * For top-level conjuncts of the form
     * ((r1+r2+r3) & (r4+r5)) in none
     * record that (r1,r4), (r1,r5) etc are disjoint.
     */
    public void visit(ElemFormula elemFormula_) {
	if (elemFormula_.getLeft() instanceof BinaryExpr &&
	    elemFormula_.getRight() instanceof EmptySetExpr) {
	    BinaryExpr left = (BinaryExpr)elemFormula_.getLeft();
	    if (left.getOp().equals(BinaryExprOp.INTERSECT)) {
		Set /* of LeafId */ leftUnion = new TreeSet();
		Set /* of LeafId */ rightUnion = new TreeSet();
		_gatherUnionLeaves(left.getLeft(), leftUnion);
		_gatherUnionLeaves(left.getLeft(), rightUnion);
		if (!leftUnion.isEmpty() && !rightUnion.isEmpty()) {
		    for (Iterator leftIter = leftUnion.iterator(); leftIter.hasNext();) {
			LeafId leftLeafId = (LeafId)leftIter.next();
			for (Iterator rightIter = rightUnion.iterator(); rightIter.hasNext();) {
			    LeafId rightLeafId = (LeafId)rightIter.next();
			    _recordAsDisjoint(leftLeafId, rightLeafId);
			    _recordAsDisjoint(rightLeafId, leftLeafId);
			}
		    }
		}
	    }
	}
    }

    /**
     * Record the fact that the two given relations are disjoint.
     */
    private void _recordAsDisjoint(LeafId id1_, LeafId id2_) {
	if (!id1_.equals(id2_)) {
	    Set /* of LeafId */ leftDisjWith = (Set)_disjWith.get(id1_);
	    if (leftDisjWith == null)
		_disjWith.put(id1_, leftDisjWith = new TreeSet());
	    leftDisjWith.add(id2_);
	}
    }
    
    /**
     * Gather relations whose values are fully contained in the given expression.
     */
    private static void _gatherUnionLeaves(Expr e_, Set /* of LeafId */ unionLeaves) {
	if (_isRelation(e_))
	    unionLeaves.add(((Leaf)e_).getLeafId());
	if (e_ instanceof BinaryExpr) {
	    BinaryExpr bexpr = (BinaryExpr)e_;
	    if (bexpr.getOp().equals(BinaryExprOp.UNION)) {
		_gatherUnionLeaves(bexpr.getLeft(), unionLeaves);
		_gatherUnionLeaves(bexpr.getRight(), unionLeaves);
	    }
	}
    }
}

